Lemma not_not_x_equals_x:
  forall b:bool, negb (negb b) = b.
Proof.
  intros.
  destruct b.
  - simpl; reflexivity.
  - simpl; reflexivity.
Qed.